|
Operational semantics are a category of formal programming language semantics in which certain desired properties of a program, such as correctness, safety or security, are verified by constructing proofs from logical statements about its execution and procedures, rather than by attaching mathematical meanings to its terms (denotational semantics). Operational semantics are classified in two categories: structural operational semantics (or small-step semantics) formally describe how the ''individual steps'' of a computation take place in a computer-based system. By opposition natural semantics (or big-step semantics) describe how the ''overall results'' of the executions are obtained. Other approaches to providing a formal semantics of programming languages include axiomatic semantics and denotational semantics. The operational semantics for a programming language describes how a valid program is interpreted as sequences of computational steps. These sequences then ''are'' the meaning of the program. In the context of functional programs, the final step in a terminating sequence returns the value of the program. (In general there can be many return values for a single program, because the program could be nondeterministic, and even for a deterministic program there can be many computation sequences since the semantics may not specify exactly what sequence of operations arrives at that value.) The concept of operational semantics was used for the first time in defining the semantics of Algol 68. The following statement is a quote from the revised ALGOL 68 report:
The first use of the term "operational semantics" in its present meaning is attributed to Dana Scott (Plotkin04). What follows is a quote from Scott's seminal paper on formal semantics, in which he mentions the "operational" aspects of semantics.
Perhaps the first formal incarnation of operational semantics was the use of the lambda calculus to define the semantics of LISP by []. Abstract machines in the tradition of the SECD machine are also closely related. == Approaches == Gordon Plotkin introduced the structural operational semantics, Robert Hieb and Matthias Felleisen the reduction contexts, and Gilles Kahn the natural semantics. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Operational semantics」の詳細全文を読む スポンサード リンク
|